Inference at * 1 0 
Iof proof for Lemma order functionality wrt iff:



1. T : Type
2. R : TT
3. R' : TT
4. x, y:T. R(x,y)  R'(x,y)
  (Refl(T;x,y.R(x,y)) & Trans(T;x,y.R(x,y)) & AntiSym(T;x,y.R(x,y)))
   (Refl(T;x,y.R'(x,y)) & Trans(T;x,y.R'(x,y)) & AntiSym(T;x,y.R'(x,y))) 

latex

 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{2:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{7:n,
 by PERMUTE{13:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{7:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n,
 by PERMUTE{19:n,
 by PERMUTE{20:n,
 by PERMUTE{21:n,
 by PERMUTE{7:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{7:n,
 by PERMUTE{22:n,
 by PERMUTE{23:n} 

latex

 1: .....wf..... NILNIL

 1:   (Refl(T;x,y.R(x,y)) & Trans(T;x,y.R(x,y)) & AntiSym(T;x,y.R(x,y)))  
 2: .....wf..... NILNIL

 2:   (Refl(T;x,y.R'(x,y)) & Trans(T;x,y.R'(x,y)) & AntiSym(T;x,y.R'(x,y)))  
 3: .....wf..... NILNIL

 3:   Refl(T;x,y.R(x,y))  
 4: .....wf..... NILNIL

 4:   Refl(T;x,y.R'(x,y))  
 5: .....wf..... NILNIL

 5:   (Trans(T;x,y.R(x,y)) & AntiSym(T;x,y.R(x,y)))  
 6: .....wf..... NILNIL

 6:   (Trans(T;x,y.R'(x,y)) & AntiSym(T;x,y.R'(x,y)))  
 7: .....wf..... NILNIL

 7:   T  Type
 8: .....wf..... NILNIL

 8:   (x,y. R(x,y))  TT
 9: .....wf..... NILNIL

 9:   (x,y. R'(x,y))  TT
 10: .....wf..... NILNIL

 10: 5. x : T
 10: 6. T
 10:   x  T
 11: .....wf..... NILNIL

 11: 5. T
 11: 6. y : T
 11:   y  T
 12: .....wf..... NILNIL

 12: 5. T
 12:   T  Type
 13: .....wf..... NILNIL

 13:   Trans(T;x,y.R(x,y))  
 14: .....wf..... NILNIL

 14:   Trans(T;x,y.R'(x,y))  
 15: .....wf..... NILNIL

 15:   AntiSym(T;x,y.R(x,y))  
 16: .....wf..... NILNIL

 16:   AntiSym(T;x,y.R'(x,y))  
 17: .....wf..... NILNIL

 17:   (y,x. R(x,y))  TT
 18: .....wf..... NILNIL

 18:   (y,x. R'(x,y))  TT
 19: .....wf..... NILNIL

 19: 5. T
 19: 6. x : T
 19:   x  T
 20: .....wf..... NILNIL

 20: 5. y : T
 20: 6. T
 20:   y  T
 21: .....wf..... NILNIL

 21: 5. T
 21:   T  Type
 22: .....wf..... NILNIL

 22:   (Refl(T;x,y.R'(x,y)) & Trans(T;x,y.R'(x,y)) & AntiSym(T;x,y.R'(x,y)))
 22:   =
 22:   (Refl(T;x,y.R'(x,y)) & Trans(T;x,y.R'(x,y)) & AntiSym(T;x,y.R'(x,y)))
 23: 

 23:   (Refl(T;x,y.R'(x,y)) & Trans(T;x,y.R'(x,y)) & AntiSym(T;x,y.R'(x,y)))
 23:    (Refl(T;x,y.R'(x,y)) & Trans(T;x,y.R'(x,y)) & AntiSym(T;x,y.R'(x,y)))
 .

Definitions	t  T, x:A  B(x), x.A(x), f(a), s = t, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), , x:AB(x), Type, x(s1,s2), x,y. t(x;y), P  Q, P  Q, P & Q, P  Q, x:A. B(x)
Lemmas	anti sym functionality wrt iff, trans functionality wrt iff, refl functionality wrt iff, and functionality wrt iff, iff functionality wrt iff